Journal
Scientific and Technical Journal of Information Technologies, Mechanics and Optics
UDK004.415.52, 004.434
Issue:6 (158)
Download PDF0 Kbyte
Specification language for automatа-based objects cooperation
Annotation
Automata-based programming is a programming paradigm that has been successfully used in the development of reactive systems, distributed control systems, and various mission-critical applications where the ability to verify the compliance of a real system with its model given in the form of specifications is critical. The traditional testing of such systems can be difficult; thus, more advanced verification tools are required to increase confidence in the reliability of real systems. The previously proposed language for the specification of the Cooperative Interaction of Automata-based Objects (CIAO) was successfully used to develop several different reactive systems as a result of which a number of shortcomings were identified and eliminated in the new version of CIAO v.3. This new version of the language was developed for the automatic verification of automata-based programs according to the formal specifications of a certain class of real-time systems. Three innovations distinguish CIAO v.3 from previous versions. First, an explicit distinction between automata classes and automaton objects as instances of these classes. Second, we specify the binding of automaton objects through interfaces using a connection scheme. Third, we describe the semantics of the behavior of a system of interacting automaton objects using a semantic graph. This paper presents the main concepts of the new language version including the abstract syntax, operational semantics, and metamodel. The third version of the CIAO language naturally includes almost all the advantages of object-oriented programming into the paradigm of automata programming. The connection of automaton objects through the corresponding interfaces is arbitrarily reflected by the connection scheme. A semantic graph describing the semantics of the behavior of the automata-based program is used to implement automatic verification with respect to formal specifications.
Keywords
Постоянный URL
Articles in current issue
- Design and fabrication of collimating ball lensed fiber for the system of optical radiation output from radiophotonic components
- From Triassic to moderinity: Raman spectroscopy for differentiation of fossil resins age by age
- Optimization of geometry of two-dimensional photonic crystal waveguide for telecommunications and sensorics
- Development and investigation of the suppressing additive noises methods in fiber-optic interferometric sensors
- Method for compensating the constant component of noise in the reflectogram of a fiber-optic communication line under conditions of insufficient dynamic range of an optical backscatter reflectometer in the time domain
- Investigation of the method of moving object weight measurement based onquasidistributed fiber Bragg gratings with temperature compensation
- Modern optical methods of non-contact geometric measurements and reconstruction of object 3D surface shape: a review
- Spectral-luminescent properties of silver clusters Ag1–5 in the ion-exchange layer of silicate glass
- Forming a thick layer of ε-Ga2O3 on the GaN sublayer with V-defects at the interface
- A model for ensuring the continuity of the safe functioning of the product quality traceability system in conditions of unstable communication
- Application of Markov chain Monte Carlo and machine learning for identifying active modules in biological graphs
- Surface defect detection with limited data based on SSD detector and Siamese networks
- Sentiment analysis of Arabic tweets using supervised machine learning (in English)
- Russian parametric corpus RuParam
- Comparative analysis of AI-generated and original abstracts of academic articles on philology
- Enhancing Kubernetes security with machine learning: а proactive approach to anomaly detection
- Prompt-based multi-task learning for robust text retrieval
- Improving question answering in programming domain with pretrained language model finetuning using structured diverse online forum data
- Aspects of organizing game interactions among asymmetric agents using graph neural networks
- Development and modeling of technological scheme of steam methane reforming with oxy-fuel combustion and carbon capture
- Stability study of hybrid MOS memristor memory using modified particle swarm optimization method
- Analysis of the vulnerability of YOLO neural network models to the Fast Sign Gradient Method attack